$\forall$$A$:Type, $x$:(Top + $A$), $a$:Atom1. $x$:Top + $A$$\parallel$$a$ $\Rightarrow$ ($\neg$($\uparrow$isl($x$))) $\Rightarrow$ outr($x$):$A$$\parallel$$a$